Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Adapt to https://github.com/coq/coq/pull/19530 #1957

Merged
merged 1 commit into from
Sep 19, 2024
Merged

Adapt to https://github.com/coq/coq/pull/19530 #1957

merged 1 commit into from
Sep 19, 2024

Conversation

proux01
Copy link
Contributor

@proux01 proux01 commented Sep 17, 2024

Adapt to coq/coq#19530
This should be backward compatible and can be merged at your convenience, before the upstream PR.

@JasonGross JasonGross enabled auto-merge (squash) September 17, 2024 06:16
@proux01 proux01 mentioned this pull request Sep 17, 2024
Merged
43 tasks
@JasonGross
Copy link
Collaborator

@proux01

File "./src/Bedrock/End2End/RupicolaCrypto/Spec.v", line 1, characters 0-29:
Error: Required library Byte matches several files in path (found
/home/coq/.opam/4.13.1+flambda/lib/coq/theories/Init/Byte.vo and
/home/coq/.opam/4.13.1+flambda/lib/coq/theories/Strings/Byte.vo).

Why not leave the intermediates (From Coq Require Import Init.Byte or similar)? That would also be more future-proof against other duplicate names

auto-merge was automatically disabled September 17, 2024 08:52

Head branch was pushed to by a user without write access

@proux01
Copy link
Contributor Author

proux01 commented Sep 17, 2024

Why not leave the intermediates (From Coq Require Import Init.Byte or similar)?

Indeed it's required for Byte, done

That would also be more future-proof against other duplicate names

There should be no other duplicates, there is a check to ensure that in the CI of the new repository.

JasonGross added a commit that referenced this pull request Sep 18, 2024
@JasonGross
Attempt to fix wasm_of_ocaml
7de7855 
As per https://github.com/ocaml-wasm/wasm_of_ocaml?tab=readme-ov-file#installation, to deal with the CI failure in #1957 / https://github.com/mit-plv/fiat-crypto/actions/runs/10906100009/job/30271149044?pr=1957
@JasonGross JasonGross mentioned this pull request Sep 18, 2024
Merged
@JasonGross
Copy link
Collaborator

Only wasm is failing, I'm working on that in #1958, #1960, let's merge

@JasonGross JasonGross merged commit 7f0f40a into mit-plv:master Sep 19, 2024
52 of 54 checks passed
@proux01
Copy link
Contributor Author

proux01 commented Sep 20, 2024

Thanks

@proux01 proux01 deleted the stdlib_repo branch September 20, 2024 07:54
JasonGross added a commit that referenced this pull request Sep 20, 2024
@JasonGross
Attempt to fix wasm_of_ocaml (#1958)
e1cc135 
* Attempt to fix wasm_of_ocaml

As per https://github.com/ocaml-wasm/wasm_of_ocaml?tab=readme-ov-file#installation, to deal with the CI failure in #1957 / https://github.com/mit-plv/fiat-crypto/actions/runs/10906100009/job/30271149044?pr=1957

* Update coq-docker.yml

* Update coq-docker.yml

Pin more than just dune as per ocaml-wasm/wasm_of_ocaml#8 (comment)

* Update coq-docker.yml
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@proux01 @JasonGross